(** ** Matrix: A Matrix Type Defined by Record *)

Require Import List.

(* ################################################################# *)
(** * Definition of Matrix Type *)

Section Mat_def.
Variable A:Set.
(** The definition of matrix type requires two relationships as support,
    one is the equivalence relationship of the height of the matrix, 
    and the second is the equivalence relationship of the width of the
    matrix.*)

(** Since we use a two-dimensional list to represent the matrix content,
    where the equivalence of the height of the matrix can be expressed 
    by the height function, the equivalence of the width of the matrix 
    can be expressed by the width function: *)

(** ** height *)
(** height returns Proposition of height relationship of two-dimensional
    list. *)
Check length.
Definition height := @length (list A).

(** ** width *)
(** width returns Proposition of width relationship of two-dimensional
    list. *)
Fixpoint width (m:list(list A)) n:=
  match m with
  | nil => True
  | a::t => (length a = n) /\ width t n (*保证每一行的元素个数，都是要和n相等的*)
  end.
(**
width [[1; 2; 3]; [2; 3; 4]; [3; 4; 5]] 3
3 = 3 /\ 3 = 3 /\ 3 = 3 /\ True

length [1; 2; 3] = 3 /\ width [2; 3; 4]; [3; 4; 5] 3
True /\ length [2; 3; 4] = 3 /\ width [3; 4; 5] 3
True /\ True /\ length [2; 3; 4] = 3 /\ width nil 3
True /\ True /\ True /\ True.
**)



(** A matrix is a type with parameters whose parameters are the number
    of rows and columns. mkMat is a function of constructing a matrix.
    The construction function requires five parameters: the number of
    rows, the number of columns, the content of the matrix, the number
    of matrix rows, and the number of matrix columns.*)

(** ** Mat *)

Record Mat (m n:nat) : Set := mkMat
  { 
    mat : list (list A);        (*the content of the matrix*)
    mat_height : height mat = m;(*一个height mat与m相等的证明*)
    mat_width : width mat n     (*一个width mat与n相等的证明*)
  }.

End Mat_def.
Arguments height {A}.
Arguments width {A}.

(** * Definition of Matrix Equality*)

(** ** M_eq *)

(** Since the matrix is defined by record, if the two matrices are
    equal and connected by an equal sign, each multiplication score in
    the two matrices is equal. However, the proof of the relationship 
    between the height and width of the matrix is not equal, so we 
    define the equality of the two-dimensional list in the matrix as
    the equality of the matrix. *)

(** Matrix equality is defined as the equality of the two-dimensional
    tables in the matrix*)
(*只需要证明矩阵里面的mat是完全一样的就可以了*)

Definition M_eq{A:Set} {m n:nat} (m1 m2:@Mat A m n ):= 
  mat A m n m1 = mat A m n m2.

(** Use the symbol === to express M_eq *)

Notation "m1 === m2" := (M_eq m1 m2) (at level 70).

(** ** Lemmas of M_eq *)

(** Proof of reflexivity of M_eq *)

Lemma M_eq_ref : forall {A:Set} {m n:nat} (m0:@Mat A m n), m0 === m0.
Proof. intros. unfold M_eq. reflexivity.
Qed.

(** Proof of symmetry of M_eq *)

Lemma M_eq_sym : forall {A:Set} {m n:nat} (m0 m1:@Mat A m n), 
  m0 === m1 -> m1 === m0.
Proof. intros. unfold M_eq in H. unfold M_eq. rewrite H. reflexivity.
Qed.

(** Proof of transitivity of M_eq *)

Lemma M_eq_trans : forall {A:Set} {m n:nat} (m0 m1 m2:@Mat A m n),
  m0 === m1 -> m1 === m2 -> m0 === m2.
Proof. intros. unfold M_eq in H. unfold M_eq in H0.
  unfold M_eq . rewrite H. rewrite <- H0. reflexivity.
Qed.

(** * Implementation of M_eq rewrite *)

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Lemma Meq_ref : forall {A:Set} {m n:nat}, reflexive _ (@M_eq A m n).
intros. unfold reflexive. apply M_eq_ref.
Qed.

Lemma Meq_sym : forall {A:Set} {m n:nat}, symmetric _ (@M_eq A m n).
intros. unfold symmetric. apply M_eq_sym.
Qed.

Lemma Meq_trans : forall {A:Set} {m n:nat}, transitive _ (@M_eq A m n).
intros. unfold transitive. apply M_eq_trans.
Qed.

Add Parametric Relation {A:Set} {m n:nat} : (@Mat A m n) (@M_eq A m n) 
  reflexivity proved by (@M_eq_ref A m n)
  symmetry proved by (@M_eq_sym A m n)
  transitivity proved by (@M_eq_trans A m n)
  as M_eq_rel.

Definition matA (A:Set)(m n:nat) := @Mat A m n.
Parameters mat_add : forall (A:Set) m n, 
  (@Mat A m n) -> (@Mat A m n ) -> (@Mat A m n) .

Axiom mat_add_compat : 
  forall (A:Set) m n, 
     forall x x' : (@Mat A m n), @M_eq A m n x x' ->
     forall y y' : (@Mat A m n), @M_eq A m n y y' ->
         @M_eq A m n (mat_add x y) (mat_add x' y').

Add Parametric Morphism {A:Set} {m n :nat}: (@mat_add A m n)
  with signature (@M_eq A m n) ==> (@M_eq A m n) ==> (@M_eq A m n) 
  as mat_add_mor.
Proof.
exact (@mat_add_compat A m n).
Qed.

Section test.
Variable A:Set.
Variable m1 m2 m3 m4 m5:@Mat A 3 3.
Axiom t1: mat_add m1 m2 === m3.
Axiom t2: m2 === mat_add m4 m5.
Lemma t3: mat_add m1 m2 === mat_add m1 (mat_add m4 m5).
Proof.
  rewrite t2. reflexivity.
Qed.
End test.
